plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
TIMES(X, s(Y)) → TIMES(Y, X)
TIMES(X, s(Y)) → PLUS(X, times(Y, X))
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TIMES(X, s(Y)) → TIMES(Y, X)
TIMES(X, s(Y)) → PLUS(X, times(Y, X))
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
The value of delta used in the strict ordering is 1/16.
POL(PLUS(x1, x2)) = (1/4)x_1
POL(plus(x1, x2)) = 1/4 + (11/4)x_1 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
TIMES(X, s(Y)) → TIMES(Y, X)
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(X, s(Y)) → TIMES(Y, X)
The value of delta used in the strict ordering is 1.
POL(TIMES(x1, x2)) = (2)x_1 + x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))